1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import topology.local_homeomorph
src └───────────────────────┘
8
9 /-!
10 # Manifolds
11
12 A manifold is a topological space M locally modelled on a model space H, i.e., the manifold is
13 covered by open subsets on which there are local homeomorphisms (the charts) going to H. If the
14 changes of charts satisfy some additional property (for instance if they are smooth), then M
15 inherits additional structure (it makes sense to talk about smooth manifolds). There are therefore
16 two different ingredients in a manifold:
17 * the set of charts, which is data
18 * the fact that changes of charts belong to some group (in fact groupoid), which is additional Prop.
19
20 We separate these two parts in the definition: the manifold structure is just the set of charts, and
21 then the different smoothness requirements (smooth manifold, orientable manifold, contact manifold,
22 and so on) are additional properties of these charts. These properties are formalized through the
23 notion of structure groupoid, i.e., a set of local homeomorphisms stable under composition and
24 inverse, to which the change of coordinates should belong.
25
26 ## Main definitions
27 * `structure_groupoid H` : a subset of local homeomorphisms of `H` stable under composition, inverse
28 and restriction (ex: local diffeos)
29 * `pregroupoid H` : a subset of local homeomorphisms of `H` stable under composition and
30 restriction, but not inverse (ex: smooth maps)
31 * `groupoid_of_pregroupoid`: construct a groupoid from a pregroupoid, by requiring that a map and its
32 inverse both belong to the pregroupoid (ex: construct diffeos from smooth
33 maps)
34 * `continuous_groupoid H` : the groupoid of all local homeomorphisms of `H`
35
36 * `manifold H M` : manifold structure on `M` modelled on `H`, given by an atlas of local
37 homeomorphisms from `M` to `H` whose sources cover `M`. This is a type class.
38 * `has_groupoid M G` : when `G` is a structure groupoid on `H` and `M` is a manifold modelled on
39 `H`, require that all coordinate changes belong to `G`. This is a type
40 class
41 * `atlas H M` : when `M` is a manifold modelled on `H`, the atlas of this manifold
42 structure, i.e., the set of charts
43 * `structomorph G M M'` : the set of diffeomorphisms between the manifolds `M` and `M'` for the
44 groupoid `G`. We avoid the word diffeomorphisms, keeping it for the
45 smooth category.
46
47 As a basic example, we give the instance
48 `instance manifold_model_space (H : Type*) [topological_space H] : manifold H H`
49 saying that a topological space is a manifold over itself, with the identity as unique chart. This
50 manifold structure is compatible with any groupoid.
51
52 ## Implementation notes
53
54 The atlas in a manifold is *not* a maximal atlas in general: the notion of maximality depends on the
55 groupoid one considers, and changing groupoids changes the maximal atlas. With the current
56 formalization, it makes sense first to choose the atlas, and then to ask whether this precise atlas
57 defines a smooth manifold, an orientable manifold, and so on. A consequence is that structomorphisms
58 between M and M' do *not* induce a bijection between the atlases of M and M': the definition is only
59 that, read in charts, the structomorphism locally belongs to the groupoid under consideration.
60 (This is equivalent to inducing a bijection between elements of the maximal atlas). A consequence
61 is that the invariance under structomorphisms of properties defined in terms of the atlas is not
62 obvious in general, and could require some work in theory (amounting to the fact that these
63 properties only depend on the maximal atlas, for instance). In practice, this does not create any
64 real difficulty.
65
66 We use the letter `H` for the model space thinking of the case of manifolds with boundary, where the
67 model space is a half space.
68
69 Manifolds are sometimes defined as topological spaces with an atlas of local diffeomorphisms, and
70 sometimes as spaces with an atlas from which a topology is deduced. We use the former approach:
71 otherwise, there would be an instance from manifolds to topological spaces, which means that any
72 instance search for topological spaces would try to find manifold structures involving a yet
73 unknown model space, leading to problems. However, we also introduce the latter approach,
74 through a structure `manifold_core` making it possible to construct a topology out of a set of local
75 equivs with compatibility conditions (but we do not register it as an instance).
76
77 In the definition of a manifold, the model space is written as an explicit parameter as there can be
78 several model spaces for a given topological space. For instance, a complex manifold (modelled over
79 ℂ^n) will also be seen sometimes as a real manifold modelled over ℝ^(2n).
80 -/
81
82 noncomputable theory
83 local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable
id └───────────────────────────┘ └──────────────────────┘
src └───────────────────────────┘ └──────────────────────┘
typ └───────────────────────────┘ └──────────────────────┘
84
85 universes u
86
87 variables {H : Type u} {M : Type*} {M' : Type*} {M'' : Type*}
88
89 /- Notational shortcut for the composition of local homeomorphisms, i.e., `local_homeomorph.trans`.
90 Note that, as is usual for equivs, the composition is from left to right, hence the direction of
91 the arrow. -/
92 local infixr ` ≫ₕ `:100 := local_homeomorph.trans
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
93
94 open set local_homeomorph
95
96 section groupoid
97
98 /- One could add to the definition of a structure groupoid the fact that the restriction of an
99 element of the groupoid to any open set still belongs to the groupoid.
100 (This is in Kobayashi-Nomizu.)
101 I am not sure I want this, for instance on H × E where E is a vector space, and the groupoid is made
102 of functions respecting the fibers and linear in the fibers (so that a manifold over this groupoid
103 is naturally a vector bundle) I prefer that the members of the groupoid are always defined on
104 sets of the form s × E
105
106 The only nontrivial requirement is locality: if a local homeomorphism belongs to the groupoid
107 around each point in its domain of definition, then it belongs to the groupoid. Without this
108 requirement, the composition of diffeomorphisms does not have to be a diffeomorphism. Note that
109 this implies that a local homeomorphism with empty source belongs to any structure groupoid, as
110 it trivially satisfies this condition.
111
112 There is also a technical point, related to the fact that a local homeomorphism is by definition a
113 global map which is a homeomorphism when restricted to its source subset (and its values outside
114 of the source are not relevant). Therefore, we also require that being a member of the groupoid only
115 depends on the values on the source.
116 -/
117 /-- A structure groupoid is a set of local homeomorphisms of a topological space stable under
118 composition and inverse. They appear in the definition of the smoothness class of a manifold. -/
119 structure structure_groupoid (H : Type u) [topological_space H] :=
id └──┘ └───────────────┘ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
120 (members : set (local_homeomorph H H))
id └─┘ └──────────────┘ ┴ ┴
src └─┘ └──────────────┘
typ └─┘ └──────────────┘ ┴ ┴
doc └──────────────┘
121 (comp : ∀e e' : local_homeomorph H H, e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ └─────┘ ┴ └┘ └┘ ┴ └─────┘
src └──────────────┘ ┴ ┴ └┘ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ └─────┘ ┴ └┘ └┘ ┴ └─────┘
doc └──────────────┘ └┘
122 (inv : ∀e : local_homeomorph H H, e ∈ members → e.symm ∈ members)
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴└───┘ ┴ └─────┘
src └──────────────┘ ┴ └───┘ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴└───┘ ┴ └─────┘
doc └──────────────┘ └───┘
123 (id_mem : local_homeomorph.refl H ∈ members)
id └───────────────────┘ ┴ ┴ └─────┘
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ └─────┘
doc └───────────────────┘
124 (locality : ∀e : local_homeomorph H H, (∀x ∈ e.source, ∃s, is_open s ∧
id ┴ └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴┴┴ └─────┘ ┴ ┴
src └──────────────┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴└─────┘ ┴┴┴ └─────┘ ┴ ┴
doc └──────────────┘ └─────┘
125 x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
id ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘
src ┴ ┴ └────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘
doc └────┘
126 (eq_on_source : ∀ e e' : local_homeomorph H H, e ∈ members → e' ≈ e → e' ∈ members)
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └┘ ┴ └─────┘
src └──────────────┘ ┴ ┴ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴ └┘ ┴ └─────┘
doc └──────────────┘
127
128 variable [topological_space H]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
129
130 @[reducible] instance : has_mem (local_homeomorph H H) (structure_groupoid H) :=
id └─────┘ └──────────────┘ ┴ ┴ └────────────────┘ ┴
src └─────┘ └──────────────┘ └────────────────┘
typ └─────┘ └──────────────┘ ┴ ┴ └────────────────┘ ┴
doc └───────┘ └──────────────┘ └────────────────┘
131 ⟨λ(e : local_homeomorph H H) (G : structure_groupoid H), e ∈ G.members⟩
id └──────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴└──────┘
src └──────────────┘ └────────────────┘ ┴ └──────┘
typ └──────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴└──────┘
doc └──────────────┘ └────────────────┘
132
133 /-- Partial order on the set of groupoids, given by inclusion of the members of the groupoid -/
134 instance structure_groupoid.partial_order : partial_order (structure_groupoid H) :=
id └───────────┘ └────────────────┘ ┴
src └───────────┘ └────────────────┘
typ └───────────┘ └────────────────┘ ┴
doc └────────────────┘
135 partial_order.lift structure_groupoid.members
id └────────────────┘ └────────────────────────┘
src └────────────────┘ └────────────────────────┘
typ └────────────────┘ └────────────────────────┘
136 (λa b h, by { cases a, cases b, dsimp at h, induction h, refl }) (by apply_instance)
id ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └────┘ └────────┘ └────────┘ └───┘ └────────────┘
typ ┴ ┴ ┴ └────┘┴ └────┘┴ └────────┘ └────────┘┴ └───┘ └────────────┘
doc └────┘ └────┘ └────────┘ └────────┘ └───┘ └────────────┘
txt └────┘ └────┘ └────────┘ └────────┘ └───┘ └────────────┘
par └────┘ └────┘ └────────┘ └────────┘ └───┘ └────────────┘
pid ┴ ┴ ┴└──┘ ┴ ┴
st └────────┘└───────┘└──────────┘└───────────┘└─────┘└┘ └─────────────┘
137
138 /-- The trivial groupoid, containing only the identity (and maps with empty source, as this is
139 necessary from the definition) -/
140 def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
id └───────────────┘ ┴ └────────────────┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ ┴ └────────────────┘ ┴
doc └───────────────┘ └────────────────┘
141 { members := {local_homeomorph.refl H} ∪ {e : local_homeomorph H H | e.source = ∅},
id ┴└───────────────────┘ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴└─────┘ ┴ ┴
src ┴└───────────────────┘ ┴ ┴ └──────────────┘ └─────┘ ┴ ┴
typ ┴└───────────────────┘ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴└─────┘ ┴ ┴
doc └───────────────────┘ └──────────────┘
142 comp := λe e' he he', begin
id ┴ └┘ └┘ └─┘
typ ┴ └┘ └┘ └─┘
st └─────
143 cases he; simp at he he',
id └┘
src └────┘ └────────────┘
typ └────┘└┘ └────────────┘
doc └────┘ └────────────┘
txt └────┘ └────────────┘
par └────┘ └────────────┘
pid ┴ ┴└───────┘
st ───────────────────────────┘└─
144 { simpa [he] },
id └┘
src └─────┘ └┘
typ └─────┘└┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴┴ ┴┴
st ─────┘└─────────┘└┘└
145 { have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _,
id └┘ └┘ ┴ └──────┘ └────────┘
src └─────┘ ┴└┘┴ └───────┘┴┴└──────┘└──┘└────────┘└──┘
typ └─────┘ ┴└┘┴└┘└───────┘┴┴└──────┘└──┘└────────┘└──┘
doc └─────┘ ┴└┘┴ └───────┘ ┴ └──┘ └──┘
txt └─────┘ ┴ ┴ └───────┘ ┴ └──┘ └──┘
par └─────┘ ┴ ┴ └───────┘ ┴ └──┘ └──┘
pid └───┘└┘ ┴ ┴ └───────┘ ┴ └──┘ └──┘
st ─────────────────────────────────────────────────────────┘└─
146 rw he at this,
id └┘
src └─┘ └──────┘
typ └─┘└┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────┘└─
147 have : (e ≫ₕ e') ∈ {e : local_homeomorph H H | e.source = ∅} := disjoint_iff.1 this,
id ┴ └┘ ┴ ┴ └──────────────┘ ┴ └─────┘ ┴ ┴ └──────────┘ └──┘
src └─────┘ ┴ ┴ └┘┴┴┴└──┘└──────────────┘┴ ┴ └─┘ └─────┘┴┴┴┴└───┘└──────────┘└─┘
typ └─────┘ ┴┴ ┴└┘└┘┴┴┴└──┘└──────────────┘┴ ┴┴└─┘ └─────┘┴┴┴┴└───┘└──────────┘└─┘└──┘
doc └─────┘ ┴ ┴ └┘ ┴ └──┘└──────────────┘┴ ┴ └─┘ ┴ ┴ └───┘ └─┘
txt └─────┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └───┘ └─┘
par └─────┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └───┘ └─┘
pid └───┘└┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ └─┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
148 exact (mem_union _ _ _).2 (or.inr this) },
id └───────┘ └────┘ └──┘
src └────┘ └───────┘└────────┘ └────┘┴ └┘
typ └────┘ └───────┘└────────┘ └────┘┴└──┘└┘
doc └────┘ └────────┘ ┴ └┘
txt └────┘ └────────┘ ┴ └┘
par └────┘ └────────┘ ┴ └┘
pid ┴ └────────┘ ┴ ┴┴
st ─────────────────────────────────────────────┘└──
149 end,
st ────┘
150 inv := λe he, begin
id ┴ └┘
typ ┴ └┘
st └─────
151 cases (mem_union _ _ _).1 he with E E,
id └───────┘ └┘
src └────┘ └───────┘└────────┘ └───────┘
typ └────┘ └───────┘└────────┘└┘└───────┘
doc └────┘ └────────┘ └───────┘
txt └────┘ └────────┘ └───────┘
par └────┘ └────────┘ └───────┘
pid ┴ └────────┘ └───────┘
st ────────────────────────────────────────┘└─
152 { finish },
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ─────┘└─────┘└┘└
153 { right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
154 simpa [e.to_local_equiv.image_source_eq_target.symm] using E },
id ┴
src └─────┘ └──────┘ ┴
typ └─────┘└──────────────────────────────────────────┘└──────┘┴┴
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────────────┘└──
155 end,
st ────┘
156 id_mem := mem_union_left _ (mem_insert _ ∅),
id └────────────┘ └────────┘ ┴
src └────────────┘ └────────┘ ┴
typ └────────────┘ └────────┘ ┴
157 locality := λe he, begin
id ┴ └┘
typ ┴ └┘
st └─────
158 cases e.source.eq_empty_or_nonempty with h h,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└───────┘
typ └────┘└───────────────────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ───────────────────────────────────────────────┘└─
159 { right, exact h },
id ┴
src └───┘ └────┘ ┴
typ └───┘ └────┘┴┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st ─────┘└───┘└────────┘└┘└
160 { left,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────────┘└─
161 rcases h with ⟨x, hx⟩,
id ┴
src └─────┘ └───────────┘
typ └─────┘┴└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ──────────────────────────┘└─
162 rcases he x hx with ⟨s, open_s, xs, hs⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └───────────────────────┘
st ────────────────────────────────────────────┘└─
163 have x's : x ∈ (e.restr s).source,
id ┴ └─────┘ ┴
src └─────────┘ ┴ ┴ └─────┘┴ └──────┘
typ └─────────┘┴┴ ┴ └─────┘┴┴└──────┘
doc └─────────┘ ┴ ┴ └─────┘┴ └──────┘
txt └─────────┘ ┴ ┴ ┴ └──────┘
par └─────────┘ ┴ ┴ ┴ └──────┘
pid └──────┘└─┘ ┴ ┴ ┴ └─────┘┴
st ──────────────────────────────────────┘└─
164 { rw [restr_source, interior_eq_of_open open_s],
id └──────────┘ └─────────────────┘ └────┘
src └──┘└──────────┘└┘└─────────────────┘┴ ┴
typ └──┘└──────────┘└┘└─────────────────┘┴└────┘┴
doc └──┘ └┘ ┴ ┴
txt └──┘ └┘ ┴ ┴
par └──┘ └┘ ┴ ┴
pid └┘ └┘ ┴ ┴
st ───────┘└──────────────┘└──────────────────────────┘└──
165 exact ⟨hx, xs⟩ },
id └┘ └┘
src └────┘ └┘ └┘
typ └────┘ └┘└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ──────────────────────┘└┘└
166 cases hs,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
167 { replace hs : local_homeomorph.restr e s = local_homeomorph.refl H,
id └────────────────────┘ ┴ ┴ └───────────────────┘ ┴
src └───────────┘└────────────────────┘┴ ┴ ┴ ┴└───────────────────┘┴
typ └───────────┘└────────────────────┘┴┴┴┴┴ ┴└───────────────────┘┴┴
doc └───────────┘└────────────────────┘┴ ┴ ┴ ┴└───────────────────┘┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └─┘└─┘ ┴ ┴ ┴ ┴ ┴
st ───────┘└───────────────────────────────────────────────────────────────┘
168 by simpa using hs,
id └┘
src └──────────┘
typ └──────────┘└┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └─
169 have : (e.restr s).source = univ, by { rw hs, simp },
id └─────┘ ┴ └──┘ └┘
src └─────┘ └─────┘┴ └───────┘ ┴└──┘ └─┘ └───┘
typ └─────┘ └─────┘┴┴└───────┘ ┴└──┘ └─┘└┘ └───┘
doc └─────┘ └─────┘┴ └───────┘ ┴ └─┘ └───┘
txt └─────┘ ┴ └───────┘ ┴ └─┘ └───┘
par └─────┘ ┴ └───────┘ ┴ └─┘ └───┘
pid └───┘└┘ ┴ └───────┘ ┴ ┴ ┴
st ───────────────────────────────────────┘ ┴└────┘└─────┘└┘└
170 change (e.to_local_equiv).source ∩ interior s = univ at this,
id └──────────────┘ ┴ └──────┘ ┴ └──┘
src └─────┘ └──────────────┘└───────┘┴┴└──────┘┴ ┴ ┴└──┘└──────┘
typ └─────┘ └──────────────┘└───────┘┴┴└──────┘┴┴┴ ┴└──┘└──────┘
doc └─────┘ └───────┘ ┴└──────┘┴ ┴ ┴ └──────┘
txt └─────┘ └───────┘ ┴ ┴ ┴ ┴ └──────┘
par └─────┘ └───────┘ ┴ ┴ ┴ ┴ └──────┘
pid ┴ └───────┘ ┴ ┴ ┴ ┴ ┴└─────┘
st ───────────────────────────────────────────────────────────────────┘└─
171 have : univ ⊆ interior s, by { rw ← this, exact inter_subset_right _ _ },
id └──┘ └──────┘ ┴ └──┘ └────────────────┘
src └─────┘└──┘┴ ┴└──────┘┴ └───┘ └────┘└────────────────┘└───┘
typ └─────┘└──┘┴ ┴└──────┘┴┴ └───┘└──┘ └────┘└────────────────┘└───┘
doc └─────┘ ┴ ┴└──────┘┴ └───┘ └────┘ └───┘
txt └─────┘ ┴ ┴ ┴ └───┘ └────┘ └───┘
par └─────┘ ┴ ┴ ┴ └───┘ └────┘ └───┘
pid └───┘└┘ ┴ ┴ ┴ └─┘ ┴ └──┘┴
st ───────────────────────────────┘ ┴└────────┘└─────────────────────────────┘└┘└
172 have : s = univ, by rwa [interior_eq_of_open open_s, univ_subset_iff] at this,
id ┴ └──┘ └─────────────────┘ └────┘ └─────────────┘
src └─────┘ ┴ ┴└──┘ └───┘└─────────────────┘┴ └┘└─────────────┘└───────┘
typ └─────┘┴┴ ┴└──┘ └───┘└─────────────────┘┴└────┘└┘└─────────────┘└───────┘
doc └─────┘ ┴ ┴ └───┘ ┴ └┘ └───────┘
txt └─────┘ ┴ ┴ └───┘ ┴ └┘ └───────┘
par └─────┘ ┴ ┴ └───┘ ┴ └┘ └───────┘
pid └───┘└┘ ┴ ┴ └┘ ┴ └┘ ┴└──────┘
st ──────────────────────┘ └────────────────────────┘└───────────────┘┴ └─
173 simpa [this, restr_univ] using hs },
id └──┘ └────────┘ └┘
src └─────┘ └┘└────────┘└──────┘ ┴
typ └─────┘└──┘└┘└────────┘└──────┘└┘┴
doc └─────┘ └┘ └──────┘ ┴
txt └─────┘ └┘ └──────┘ ┴
par └─────┘ └┘ └──────┘ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴
st ─────────────────────────────────────────┘└┘└
174 { exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ──────────────┘└─
175 rw mem_set_of_eq at hs,
id └───────────┘
src └─┘└───────────┘└────┘
typ └─┘└───────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ─────────────────────────────┘└─
176 rwa hs at x's } },
id └┘
src └──┘ └──────┘
typ └──┘└┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid ┴ └─────┘┴
st ─────────────────────┘└────
177 end,
st ────┘
178 eq_on_source := λe e' he he'e, begin
id ┴ └┘ └┘ └──┘
typ ┴ └┘ └┘ └──┘
st └─────
179 cases he,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
180 { left,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└──┘└─
181 have : e = e',
id ┴ └┘
src └─────┘ ┴ ┴
typ └─────┘┴┴ ┴└┘
doc └─────┘ ┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴
st ──────────────────┘└─
182 { refine eq_of_eq_on_source_univ (setoid.symm he'e) _ _;
id └─────────────────────┘ └─────────┘ └──┘
src └─────┘└─────────────────────┘┴ └─────────┘┴ └───┘
typ └─────┘└─────────────────────┘┴ └─────────┘┴└──┘└───┘
doc └─────┘ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ └───┘
par └─────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └───┘
st ───────┘└──────────────────────────────────────────────────────
183 rw set.mem_singleton_iff.1 he ; refl },
id └───────────────────┘ └┘
src └─┘└───────────────────┘└─┘ ┴ └───┘
typ └─┘└───────────────────┘└─┘└┘┴ └───┘
doc └─┘ └─┘ ┴ └───┘
txt └─┘ └─┘ ┴ └───┘
par └─┘ └─┘ ┴ └───┘
pid ┴ └─┘ ┴ ┴
st ──────────┘└───────────────────┘└───────────┘└┘└
184 rwa ← this },
id └──┘
src └────┘ ┴
typ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └─┘ ┴
st ────────────────┘└┘└
185 { right,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
186 change (e.to_local_equiv).source = ∅ at he,
id └──────────────┘
src └─────┘ └──────────────┘└───────┘ ┴ └────┘
typ └─────┘ └──────────────┘└───────┘ ┴ └────┘
doc └─────┘ └───────┘ ┴ └────┘
txt └─────┘ └───────┘ ┴ └────┘
par └─────┘ └───────┘ ┴ └────┘
pid ┴ └───────┘ ┴ ┴└───┘
st ───────────────────────────────────────────────┘└─
187 rwa [set.mem_set_of_eq, source_eq_of_eq_on_source he'e] }
id └───────────────┘ └───────────────────────┘ └──┘
src └───┘└───────────────┘└┘└───────────────────────┘┴ └┘
typ └───┘└───────────────┘└┘└───────────────────────┘┴└──┘└┘
doc └───┘ └┘└───────────────────────┘┴ └┘
txt └───┘ └┘ ┴ └┘
par └───┘ └┘ ┴ └┘
pid └┘ └┘ ┴ ┴┴
st ───────────────────────────┘└──────────────────────────────┘┴┴└─
188 end }
st ────┘
189
190 /-- Every structure groupoid contains the identity groupoid -/
191 instance : lattice.order_bot (structure_groupoid H) :=
id └───────────────┘ └────────────────┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ └────────────────┘ ┴
doc └───────────────┘ └────────────────┘
192 { bot := id_groupoid H,
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
193 bot_le := begin
st └─────
194 assume u f hf,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ────────────────┘└─
195 change f ∈ {local_homeomorph.refl H} ∪ {e : local_homeomorph H H | e.source = ∅} at hf,
id ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─────┘ ┴ ┴
src └─────┘ ┴┴┴┴└────────────────────┘ └┘┴┴┴└──┘└──────────────┘┴ ┴ └─┘ └─────┘┴┴┴┴└─────┘
typ └─────┘┴┴┴┴┴└────────────────────┘ └┘┴┴┴└──┘└──────────────┘┴ ┴┴└─┘ └─────┘┴┴┴┴└─────┘
doc └─────┘ ┴ ┴ └────────────────────┘ └┘ ┴ └──┘└──────────────┘┴ ┴ └─┘ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ └────────────────────┘ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ └────────────────────┘ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └────────────────────┘ └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴┴└───┘
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
196 simp only [singleton_union, mem_set_of_eq, mem_insert_iff] at hf,
id └─────────────┘ └───────────┘ └────────────┘
src └─────────┘└─────────────┘└┘└───────────┘└┘└────────────┘└─────┘
typ └─────────┘└─────────────┘└┘└───────────┘└┘└────────────┘└─────┘
doc └─────────┘ └┘ └┘ └─────┘
txt └─────────┘ └┘ └┘ └─────┘
par └─────────┘ └┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ └┘ ┴┴└───┘
st ───────────────────────────────────────────────────────────────────┘└─
197 cases hf,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
198 { rw hf,
id └┘
src └─┘
typ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└───┘└─
199 apply u.id_mem },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────┘└┘└
200 { apply u.locality,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
201 assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────────┘└─
202 rw [hf, mem_empty_eq] at hx,
id └┘ └──────────┘
src └──┘ └┘└──────────┘└─────┘
typ └──┘└┘└┘└──────────┘└─────┘
doc └──┘ └┘ └─────┘
txt └──┘ └┘ └─────┘
par └──┘ └┘ └─────┘
pid └┘ └┘ ┴└────┘
st ───────────┘└────────────┘┴└────┘└─
203 exact hx.elim }
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘└─
204 end,
st ────┘
205 ..structure_groupoid.partial_order }
id └──────────────────────────────┘
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
206
207 /-- To construct a groupoid, one may consider classes of local homeos such that both the function
208 and its inverse have some property. If this property is stable under composition,
209 one gets a groupoid. `pregroupoid` bundles the properties needed for this construction, with the
210 groupoid of smooth functions with smooth inverses as an application. -/
211 structure pregroupoid (H : Type*) [topological_space H] :=
id └───┘ └───────────────┘ ┴
src └───────────────┘
typ └───┘ └───────────────┘ ┴
doc └───────────────┘
212 (property : (H → H) → (set H) → Prop)
id ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴
213 (comp : ∀{f g u v}, property f u → property g v → is_open (u ∩ f ⁻¹' v)
id ┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ ┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └─┘ ┴
doc └─────┘ └─┘
214 → property (g ∘ f) (u ∩ f ⁻¹' v))
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴ └─┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘
215 (id_mem : property id univ)
id └──────┘ └┘ └──┘
src └┘ └──┘
typ └──────┘ └┘ └──┘
216 (locality : ∀{f u}, is_open u → (∀x∈u, ∃v, is_open v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u)
id ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
typ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘ └─────┘
217 (congr : ∀{f g : H → H} {u}, is_open u → (∀x∈u, g x = f x) → property f u → property g u)
id ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘
218
219 /-- Construct a groupoid of local homeos for which the map and its inverse have some property,
220 from a pregroupoid asserting that this property is stable under composition. -/
221 def pregroupoid.groupoid (PG : pregroupoid H) : structure_groupoid H :=
id └─────────┘ ┴ └────────────────┘ ┴
src └─────────┘ └────────────────┘
typ └─────────┘ ┴ └────────────────┘ ┴
doc └─────────┘ └────────────────┘
222 { members := {e : local_homeomorph H H | PG.property e.to_fun e.source ∧ PG.property e.inv_fun e.target},
id ┴ └──────────────┘ ┴ ┴ └┘└───────┘ ┴└─────┘ ┴└─────┘ ┴ └┘└───────┘ ┴└──────┘ ┴└─────┘
src ┴ └──────────────┘ └───────┘ └─────┘ └─────┘ ┴ └───────┘ └──────┘ └─────┘
typ ┴ └──────────────┘ ┴ ┴ └┘└───────┘ ┴└─────┘ ┴└─────┘ ┴ └┘└───────┘ ┴└──────┘ ┴└─────┘
doc └──────────────┘
223 comp := λe e' he he', begin
id ┴ └┘ └┘ └─┘
typ ┴ └┘ └┘ └─┘
st └─────
224 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
225 { apply PG.comp he.1 he'.1,
id └─────┘ └┘ └─┘
src └────┘└─────┘┴ └─┘ └┘
typ └────┘└─────┘┴└┘└─┘└─┘└┘
doc └────┘ ┴ └─┘ └┘
txt └────┘ ┴ └─┘ └┘
par └────┘ ┴ └─┘ └┘
pid ┴ ┴ └─┘ └┘
st ─────┘└──────────────────────┘└─
226 apply e.continuous_to_fun.preimage_open_of_open e.open_source e'.open_source },
id └───────────────────────────────────────┘ └───────────┘ └────────────┘
src └────┘└───────────────────────────────────────┘┴└───────────┘┴└────────────┘┴
typ └────┘└───────────────────────────────────────┘┴└───────────┘┴└────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└┘└
227 { apply PG.comp he'.2 he.2,
id └─────┘ └─┘ └┘
src └────┘└─────┘┴ └─┘ └┘
typ └────┘└─────┘┴└─┘└─┘└┘└┘
doc └────┘ ┴ └─┘ └┘
txt └────┘ ┴ └─┘ └┘
par └────┘ ┴ └─┘ └┘
pid ┴ ┴ └─┘ └┘
st ─────────────────────────────┘└─
228 apply e'.continuous_inv_fun.preimage_open_of_open e'.open_target e.open_target }
id └─────────────────────────────────────────┘ └────────────┘ └───────────┘
src └────┘└─────────────────────────────────────────┘┴└────────────┘┴└───────────┘┴
typ └────┘└─────────────────────────────────────────┘┴└────────────┘┴└───────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
229 end,
st ────┘
230 inv := λe he, ⟨he.2, he.1⟩,
id ┴ └┘ └┘┴ └┘┴
src ┴ ┴
typ ┴ └┘ └┘┴ └┘┴
231 id_mem := ⟨PG.id_mem, PG.id_mem⟩,
id └┘└─────┘ └┘└─────┘
src └─────┘ └─────┘
typ └┘└─────┘ └┘└─────┘
232 locality := λe he, begin
id ┴ └┘
typ ┴ └┘
st └─────
233 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
234 { apply PG.locality e.open_source (λx xu, _),
id └─────────┘ └───────────┘
src └────┘└─────────┘┴└───────────┘┴ └──────┘
typ └────┘└─────────┘┴└───────────┘┴ └──────┘
doc └────┘ ┴ ┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ─────┘└────────────────────────────────────────┘└─
235 rcases he x xu with ⟨s, s_open, xs, hs⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └───────────────────────┘
st ────────────────────────────────────────────┘└─
236 refine ⟨s, s_open, xs, _⟩,
id ┴ └────┘ └┘
src └─────┘ └┘ └┘ └──┘
typ └─────┘ ┴└┘└────┘└┘└┘└──┘
doc └─────┘ └┘ └┘ └──┘
txt └─────┘ └┘ └┘ └──┘
par └─────┘ └┘ └┘ └──┘
pid ┴ └┘ └┘ └──┘
st ──────────────────────────────┘└─
237 convert hs.1,
id └┘
src └──────┘ └┘
typ └──────┘└┘└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid ┴ └┘
st ─────────────────┘└─
238 exact (interior_eq_of_open s_open).symm },
id └─────────────────┘ └────┘
src └────┘ └─────────────────┘┴ └─────┘
typ └────┘ └─────────────────┘┴└────┘└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ─────────────────────────────────────────────┘└┘└
239 { apply PG.locality e.open_target (λx xu, _),
id └─────────┘ └───────────┘
src └────┘└─────────┘┴└───────────┘┴ └──────┘
typ └────┘└─────────┘┴└───────────┘┴ └──────┘
doc └────┘ ┴ ┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ───────────────────────────────────────────────┘└─
240 rcases he (e.inv_fun x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩,
id └┘ └───────┘ ┴ └──────────┘ └┘
src └─────┘ ┴ └───────┘┴ └┘ └──────────┘┴ └────────────────────────┘
typ └─────┘└┘┴ └───────┘┴┴└┘ └──────────┘┴└┘└────────────────────────┘
doc └─────┘ ┴ ┴ └┘ ┴ └────────────────────────┘
txt └─────┘ ┴ ┴ └┘ ┴ └────────────────────────┘
par └─────┘ ┴ ┴ └┘ ┴ └────────────────────────┘
pid ┴ ┴ ┴ └┘ ┴ └────────────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
241 refine ⟨e.target ∩ e.inv_fun ⁻¹' s, _, ⟨xu, xs⟩, _⟩,
id └──────┘ ┴ └───────┘ └─┘ ┴ └┘ └┘
src └─────┘ └──────┘┴┴┴└───────┘┴└─┘┴ └───┘ └┘ └───┘
typ └─────┘ └──────┘┴┴┴└───────┘┴└─┘┴┴└───┘ └┘└┘└┘└───┘
doc └─────┘ ┴ ┴ ┴└─┘┴ └───┘ └┘ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ └───┘ └┘ └───┘
par └─────┘ ┴ ┴ ┴ ┴ └───┘ └┘ └───┘
pid ┴ ┴ ┴ ┴ ┴ └───┘ └┘ └───┘
st ────────────────────────────────────────────────────────┘└─
242 { exact continuous_on.preimage_open_of_open e.continuous_inv_fun e.open_target s_open },
id └─────────────────────────────────┘ └──────────────────┘ └───────────┘ └────┘
src └────┘└─────────────────────────────────┘┴└──────────────────┘┴└───────────┘┴ ┴
typ └────┘└─────────────────────────────────┘┴└──────────────────┘┴└───────────┘┴└────┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────┘└──────────────────────────────────────────────────────────────────────────────────┘└┘└
243 { rw [← inter_assoc, inter_self],
id └─────────┘ └────────┘
src └────┘└─────────┘└┘└────────┘┴
typ └────┘└─────────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ────────────────────────┘└──────────┘└──
244 convert hs.2,
id └┘
src └──────┘ └┘
typ └──────┘└┘└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid ┴ └┘
st ───────────────────┘└─
245 exact (interior_eq_of_open s_open).symm } },
id └─────────────────┘ └────┘
src └────┘ └─────────────────┘┴ └─────┘
typ └────┘ └─────────────────┘┴└────┘└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ───────────────────────────────────────────────┘└────
246 end,
st ────┘
247 eq_on_source := λe e' he ee', begin
id ┴ └┘ └┘ └─┘
typ ┴ └┘ └┘ └─┘
st └─────
248 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
249 { apply PG.congr e'.open_source ee'.2,
id └──────┘ └────────────┘ └─┘
src └────┘└──────┘┴└────────────┘┴ └┘
typ └────┘└──────┘┴└────────────┘┴└─┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
st ─────┘└─────────────────────────────────┘└─
250 simp only [ee'.1, he.1] },
id └─┘ └┘
src └─────────┘ └──┘ └──┘
typ └─────────┘└─┘└──┘└┘└──┘
doc └─────────┘ └──┘ └──┘
txt └─────────┘ └──┘ └──┘
par └─────────┘ └──┘ └──┘
pid ┴└──┘└┘ └──┘ └─┘┴
st ─────────────────────────────┘└┘└
251 { have A := eq_on_source_symm ee',
id └───────────────┘ └─┘
src └────────┘└───────────────┘┴
typ └────────┘└───────────────┘┴└─┘
doc └────────┘└───────────────┘┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ────────────────────────────────────┘└─
252 apply PG.congr e'.symm.open_source A.2,
id └──────┘ └─────────────────┘ ┴
src └────┘└──────┘┴└─────────────────┘┴ └┘
typ └────┘└──────┘┴└─────────────────┘┴┴└┘
doc └────┘ ┴└─────────────────┘┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
253 convert he.2,
id └┘
src └──────┘ └┘
typ └──────┘└┘└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid ┴ └┘
st ─────────────────┘└─
254 rw A.1,
id ┴
src └─┘ └┘
typ └─┘┴└┘
doc └─┘ └┘
txt └─┘ └┘
par └─┘ └┘
pid ┴ └┘
st ───────────┘└─
255 refl }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└─
256 end }
st ────┘
257
258 lemma mem_groupoid_of_pregroupoid (PG : pregroupoid H) (e : local_homeomorph H H) :
id └─────────┘ ┴ └──────────────┘ ┴ ┴
src └─────────┘ └──────────────┘
typ └─────────┘ ┴ └──────────────┘ ┴ ┴
doc └─────────┘ └──────────────┘
259 e ∈ PG.groupoid ↔ PG.property e.to_fun e.source ∧ PG.property e.inv_fun e.target :=
id ┴ ┴ └┘└───────┘ ┴ └┘└───────┘ ┴└─────┘ ┴└─────┘ ┴ └┘└───────┘ ┴└──────┘ ┴└─────┘
src ┴ └───────┘ ┴ └───────┘ └─────┘ └─────┘ ┴ └───────┘ └──────┘ └─────┘
typ ┴ ┴ └┘└───────┘ ┴ └┘└───────┘ ┴└─────┘ ┴└─────┘ ┴ └┘└───────┘ ┴└──────┘ ┴└─────┘
doc └───────┘
260 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
261
262 lemma groupoid_of_pregroupoid_le (PG₁ PG₂ : pregroupoid H)
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
263 (h : ∀f s, PG₁.property f s → PG₂.property f s) :
id ┴ ┴ └─┘└───────┘ ┴ ┴ └─┘└───────┘ ┴ ┴
src └───────┘ └───────┘
typ ┴ ┴ └─┘└───────┘ ┴ ┴ └─┘└───────┘ ┴ ┴
264 PG₁.groupoid ≤ PG₂.groupoid :=
id └─┘└───────┘ ┴ └─┘└───────┘
src └───────┘ ┴ └───────┘
typ └─┘└───────┘ ┴ └─┘└───────┘
doc └───────┘ └───────┘
265 begin
st └─────
266 assume e he,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
267 rw mem_groupoid_of_pregroupoid at he ⊢,
id └─────────────────────────┘
src └─┘└─────────────────────────┘└──────┘
typ └─┘└─────────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ───────────────────────────────────────┘└─
268 exact ⟨h _ _ he.1, h _ _ he.2⟩
id ┴ └┘
src └────┘ └───┘ └──┘ └───┘ └──┘
typ └────┘ └───┘ └──┘┴└───┘└┘└──┘
doc └────┘ └───┘ └──┘ └───┘ └──┘
txt └────┘ └───┘ └──┘ └───┘ └──┘
par └────┘ └───┘ └──┘ └───┘ └──┘
pid ┴ └───┘ └──┘ └───┘ └─┘┴
st ────────────────────────────────┘
269 end
st └─┘
270
271 lemma mem_pregroupoid_of_eq_on_source (PG : pregroupoid H) {e e' : local_homeomorph H H}
id └─────────┘ ┴ └──────────────┘ ┴ ┴
src └─────────┘ └──────────────┘
typ └─────────┘ ┴ └──────────────┘ ┴ ┴
doc └─────────┘ └──────────────┘
272 (he' : e ≈ e') (he : PG.property e.to_fun e.source) :
id ┴ ┴ └┘ └┘└───────┘ ┴└─────┘ ┴└─────┘
src ┴ └───────┘ └─────┘ └─────┘
typ ┴ ┴ └┘ └┘└───────┘ ┴└─────┘ ┴└─────┘
273 PG.property e'.to_fun e'.source :=
id └┘└───────┘ └┘└─────┘ └┘└─────┘
src └───────┘ └─────┘ └─────┘
typ └┘└───────┘ └┘└─────┘ └┘└─────┘
274 begin
st └─────
275 rw ← he'.1,
id └─┘
src └───┘ └┘
typ └───┘└─┘└┘
doc └───┘ └┘
txt └───┘ └┘
par └───┘ └┘
pid └─┘ └┘
st ───────────┘└─
276 exact PG.congr e.open_source (λx hx, (he'.2 x hx).symm) he,
id └──────┘ └───────────┘ └─┘ └┘
src └────┘└──────┘┴└───────────┘┴ └────┘ └─┘ ┴ └──────┘
typ └────┘└──────┘┴└───────────┘┴ └────┘ └─┘└─┘ ┴ └──────┘└┘
doc └────┘ ┴ ┴ └────┘ └─┘ ┴ └──────┘
txt └────┘ ┴ ┴ └────┘ └─┘ ┴ └──────┘
par └────┘ ┴ ┴ └────┘ └─┘ ┴ └──────┘
pid ┴ ┴ ┴ └────┘ └─┘ ┴ └──────┘
st ───────────────────────────────────────────────────────────┘└─
277 end
st ──┘
278
279 /-- The groupoid of all local homeomorphisms on a topological space H -/
280 def continuous_groupoid (H : Type*) [topological_space H] : structure_groupoid H :=
id └───────────────┘ ┴ └────────────────┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ ┴ └────────────────┘ ┴
doc └───────────────┘ └────────────────┘
281 pregroupoid.groupoid
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
282 { property := λf s, true,
id ┴ ┴ └──┘
src └──┘
typ ┴ ┴ └──┘
283 comp := λf g u v hf hg huv, trivial,
id ┴ ┴ ┴ ┴ └┘ └┘ └─┘ └─────┘
src └─────┘
typ ┴ ┴ ┴ ┴ └┘ └┘ └─┘ └─────┘
284 id_mem := trivial,
id └─────┘
src └─────┘
typ └─────┘
285 locality := λf u u_open h, trivial,
id ┴ ┴ └────┘ ┴ └─────┘
src └─────┘
typ ┴ ┴ └────┘ ┴ └─────┘
286 congr := λf g u u_open hcongr hf, trivial }
id ┴ ┴ ┴ └────┘ └────┘ └┘ └─────┘
src └─────┘
typ ┴ ┴ ┴ └────┘ └────┘ └┘ └─────┘
287
288 /-- Every structure groupoid is contained in the groupoid of all local homeomorphisms -/
289 instance : lattice.order_top (structure_groupoid H) :=
id └───────────────┘ └────────────────┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ └────────────────┘ ┴
doc └───────────────┘ └────────────────┘
290 { top := continuous_groupoid H,
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
doc └─────────────────┘
291 le_top := λ u f hf, by { split; exact dec_trivial },
id ┴ ┴ └┘ └─────────┘
src └───┘ └────┘└─────────┘┴
typ ┴ ┴ └┘ └───┘ └────┘└─────────┘┴
doc └───┘ └────┘└─────────┘┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st └──────────────────────────┘└┘
292 ..structure_groupoid.partial_order }
id └──────────────────────────────┘
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
293
294 end groupoid
295
296 /-- A manifold is a topological space endowed with an atlas, i.e., a set of local homeomorphisms
297 taking value in a model space H, called charts, such that the domains of the charts cover the whole
298 space. We express the covering property by chosing for each x a member `chart_at x` of the atlas
299 containing x in its source: in the smooth case, this is convenient to construct the tangent bundle
300 in an efficient way.
301 The model space is written as an explicit parameter as there can be several model spaces for a
302 given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen
303 sometimes as a real manifold over ℝ^(2n).
304 -/
305 class manifold (H : Type*) [topological_space H] (M : Type*) [topological_space M] :=
id └───┘ └───────────────┘ ┴ └───┘ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ └───┘ └───────────────┘ ┴ └───┘ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘
306 (atlas : set (local_homeomorph M H))
id └─┘ └──────────────┘ ┴ ┴
src └─┘ └──────────────┘
typ └─┘ └──────────────┘ ┴ ┴
doc └──────────────┘
307 (chart_at : M → local_homeomorph M H)
id ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
308 (mem_chart_source : ∀x, x ∈ (chart_at x).source)
id ┴ ┴ ┴ └──────┘ ┴ └────┘
src ┴ └────┘
typ ┴ ┴ ┴ └──────┘ ┴ └────┘
309 (chart_mem_atlas : ∀x, chart_at x ∈ atlas)
id ┴ └──────┘ ┴ ┴ └───┘
src ┴
typ ┴ └──────┘ ┴ ┴ └───┘
310
311 export manifold
312 attribute [simp] mem_chart_source chart_mem_atlas
id └──────────────┘ └─────────────┘
src └──────────────┘ └─────────────┘
typ └──────────────┘ └─────────────┘
doc └──┘
313
314 section manifold
315
316 /-- Any space is a manifold modelled over itself, by just using the identity chart -/
317 instance manifold_model_space (H : Type*) [topological_space H] : manifold H H :=
id └───────────────┘ ┴ └──────┘ ┴ ┴
src └───────────────┘ └──────┘
typ └───────────────┘ ┴ └──────┘ ┴ ┴
doc └───────────────┘ └──────┘
318 { atlas := {local_homeomorph.refl H},
id ┴└───────────────────┘ ┴
src ┴└───────────────────┘
typ ┴└───────────────────┘ ┴
doc └───────────────────┘
319 chart_at := λx, local_homeomorph.refl H,
id ┴ └───────────────────┘ ┴
src └───────────────────┘
typ ┴ └───────────────────┘ ┴
doc └───────────────────┘
320 mem_chart_source := λx, mem_univ x,
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
321 chart_mem_atlas := λx, mem_singleton _ }
id ┴ └───────────┘
src └───────────┘
typ ┴ └───────────┘
322
323 /-- In the trivial manifold structure of a space modelled over itself through the identity, the
324 atlas members are just the identity -/
325 @[simp] lemma model_space_atlas {H : Type*} [topological_space H] {e : local_homeomorph H H} :
id └───────────────┘ ┴ └──────────────┘ ┴ ┴
src └───────────────┘ └──────────────┘
typ └───────────────┘ ┴ └──────────────┘ ┴ ┴
doc └──┘ └───────────────┘ └──────────────┘
326 e ∈ atlas H H ↔ e = local_homeomorph.refl H :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴
src ┴ └───┘ ┴ ┴ └───────────────────┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴
doc └───────────────────┘
327 by simp [atlas, manifold.atlas]
src └────┘ └┘ └─
typ └────┘ └┘ └─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────────
328
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
329 /-- In the model space, chart_at is always the identity -/
330 @[simp] lemma chart_at_model_space_eq {H : Type*} [topological_space H] {x : H} :
id └───────────────┘ ┴ ┴
src └───────────────┘
typ └───────────────┘ ┴ ┴
doc └──┘ └───────────────┘
331 chart_at H x = local_homeomorph.refl H :=
id └──────┘ ┴ ┴ ┴ └───────────────────┘ ┴
src └──────┘ ┴ └───────────────────┘
typ └──────┘ ┴ ┴ ┴ └───────────────────┘ ┴
doc └───────────────────┘
332 by simpa using chart_mem_atlas H x
id └─────────────┘ ┴ ┴
src └──────────┘└─────────────┘┴ ┴ └
typ └──────────┘└─────────────┘┴┴┴┴└
doc └──────────┘ ┴ ┴ └
txt └──────────┘ ┴ ┴ └
par └──────────┘ ┴ ┴ └
pid ┴└────┘ ┴ ┴ └
st └────────────────────────────────
333
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
334 end manifold
335
336 /-- Sometimes, one may want to construct a manifold structure on a space which does not yet have
337 a topological structure, where the topology would come from the charts. For this, one needs charts
338 that are only local equivs, and continuity properties for their composition.
339 This is formalised in `manifold_core`. -/
340 structure manifold_core (H : Type*) [topological_space H] (M : Type*) :=
id └───┘ └───────────────┘ ┴ └───┘
src └───────────────┘
typ └───┘ └───────────────┘ ┴ └───┘
doc └───────────────┘
341 (atlas : set (local_equiv M H))
id └─┘ └─────────┘ ┴ ┴
src └─┘ └─────────┘
typ └─┘ └─────────┘ ┴ ┴
doc └─────────┘
342 (chart_at : M → local_equiv M H)
id ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘
typ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘
343 (mem_chart_source : ∀x, x ∈ (chart_at x).source)
id ┴ ┴ ┴ └──────┘ ┴ └────┘
src ┴ └────┘
typ ┴ ┴ ┴ └──────┘ ┴ └────┘
344 (chart_mem_atlas : ∀x, chart_at x ∈ atlas)
id ┴ └──────┘ ┴ ┴ └───┘
src ┴
typ ┴ └──────┘ ┴ ┴ └───┘
345 (open_source : ∀e e' : local_equiv M H, e ∈ atlas → e' ∈ atlas → is_open (e.symm.trans e').source)
id ┴ └─────────┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ └───┘ └─────┘ ┴└───┘└────┘ └┘ └────┘
src └─────────┘ ┴ ┴ └─────┘ └───┘└────┘ └────┘
typ ┴ └─────────┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ └───┘ └─────┘ ┴└───┘└────┘ └┘ └────┘
doc └─────────┘ └─────┘ └───┘└────┘
346 (continuous_to_fun : ∀e e' : local_equiv M H, e ∈ atlas → e' ∈ atlas →
id ┴ └─────────┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ └───┘
src └─────────┘ ┴ ┴
typ ┴ └─────────┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ └───┘
doc └─────────┘
347 continuous_on (e.symm.trans e').to_fun (e.symm.trans e').source)
id └───────────┘ ┴└───┘└────┘ └┘ └────┘ ┴└───┘└────┘ └┘ └────┘
src └───────────┘ └───┘└────┘ └────┘ └───┘└────┘ └────┘
typ └───────────┘ ┴└───┘└────┘ └┘ └────┘ ┴└───┘└────┘ └┘ └────┘
doc └───────────┘ └───┘└────┘ └───┘└────┘
348
349 namespace manifold_core
350
351 variables [topological_space H] (c : manifold_core H M) {e : local_equiv M H}
id ┴└───────────────┘ └───────────┘ └─────────┘
src └───────────────┘ └───────────┘ └─────────┘
typ ┴└───────────────┘ └───────────┘ └─────────┘
doc └───────────────┘ └───────────┘ └─────────┘
352
353 /-- Topology generated by a set of charts on a Type. -/
354 protected def to_topological_space : topological_space M :=
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
355 topological_space.generate_from $ ⋃ (e : local_equiv M H) (he : e ∈ c.atlas)
id └─────────────────────────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └─────────────────────────────┘ ┴ └─────────┘ ┴ └────┘
typ └─────────────────────────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘
doc └─────────────────────────────┘ ┴ └─────────┘
356 (s : set H) (s_open : is_open s), {e.to_fun ⁻¹' s ∩ e.source}
id └─┘ ┴ └─────┘ ┴ ┴ ┴┴└─────┘ └─┘ ┴ ┴ ┴└─────┘
src └─┘ └─────┘ ┴ ┴ └─────┘ └─┘ ┴ └─────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴┴└─────┘ └─┘ ┴ ┴ ┴└─────┘
doc └─────┘ ┴ └─┘
357
358 lemma open_source' (he : e ∈ c.atlas) : @is_open M c.to_topological_space e.source :=
id ┴ ┴ ┴└────┘ └─────┘ ┴ ┴└───────────────────┘ ┴└─────┘
src ┴ └────┘ └─────┘ └───────────────────┘ └─────┘
typ ┴ ┴ ┴└────┘ └─────┘ ┴ ┴└───────────────────┘ ┴└─────┘
doc └─────┘ └───────────────────┘
359 begin
st └─────
360 apply topological_space.generate_open.basic,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────────────────┘└─
361 simp only [exists_prop, mem_Union, mem_singleton_iff],
id └─────────┘ └───────┘ └───────────────┘
src └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘┴
typ └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────┘└─
362 refine ⟨e, he, univ, is_open_univ, _⟩,
id ┴ └┘ └──┘ └──────────┘
src └─────┘ └┘ └┘└──┘└┘└──────────┘└──┘
typ └─────┘ ┴└┘└┘└┘└──┘└┘└──────────┘└──┘
doc └─────┘ └┘ └┘ └┘ └──┘
txt └─────┘ └┘ └┘ └┘ └──┘
par └─────┘ └┘ └┘ └┘ └──┘
pid ┴ └┘ └┘ └┘ └──┘
st ──────────────────────────────────────┘└─
363 simp only [set.univ_inter, set.preimage_univ]
id └────────────┘ └───────────────┘
src └─────────┘└────────────┘└┘└───────────────┘└┘
typ └─────────┘└────────────┘└┘└───────────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ───────────────────────────────────────────────┘
364 end
st └─┘
365
366 lemma open_target (he : e ∈ c.atlas) : is_open e.target :=
id ┴ ┴ ┴└────┘ └─────┘ ┴└─────┘
src ┴ └────┘ └─────┘ └─────┘
typ ┴ ┴ ┴└────┘ └─────┘ ┴└─────┘
doc └─────┘
367 begin
st └─────
368 have E : e.target ∩ e.inv_fun ⁻¹' e.source = e.target :=
id ┴ └───────┘ └─┘ └──────┘ ┴ └──────┘
src └───────┘ ┴┴┴└───────┘┴└─┘┴└──────┘┴┴┴└──────┘└───
typ └───────┘ ┴┴┴└───────┘┴└─┘┴└──────┘┴┴┴└──────┘└───
doc └───────┘ ┴ ┴ ┴└─┘┴ ┴ ┴ └───
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ───────────────────────────────────────────────────────────
369 subset.antisymm (inter_subset_left _ _) (λx hx, ⟨hx,
id └─────────────┘ └───────────────┘
src ─┘└─────────────┘┴ └───────────────┘└────┘ └────┘ └─
typ ─┘└─────────────┘┴ └───────────────┘└────┘ └────┘ └─
doc ─┘ ┴ └────┘ └────┘ └─
txt ─┘ ┴ └────┘ └────┘ └─
par ─┘ ┴ └────┘ └────┘ └─
pid ─┘ ┴ └────┘ └────┘ └─
st ───────────────────────────────────────────────────────
370 local_equiv.target_subset_preimage_source _ hx⟩),
id └───────────────────────────────────────┘
src ───┘└───────────────────────────────────────┘└─┘ └┘
typ ───┘└───────────────────────────────────────┘└─┘ └┘
doc ───┘ └─┘ └┘
txt ───┘ └─┘ └┘
par ───┘ └─┘ └┘
pid ───┘ └─┘ └┘
st ───────────────────────────────────────────────────┘└─
371 simpa [local_equiv.trans_source, E] using c.open_source e e he he
id └──────────────────────┘ ┴ └───────────┘ ┴ └┘
src └─────┘└──────────────────────┘└┘ └──────┘└───────────┘┴ ┴ ┴ ┴ ┴
typ └─────┘└──────────────────────┘└┘┴└──────┘└───────────┘┴ ┴┴┴ ┴└┘┴
doc └─────┘ └┘ └──────┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └┘ └──────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ └┘ └──────┘ ┴ ┴ ┴ ┴ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘
372 end
st └─┘
373
374 def local_homeomorph (e : local_equiv M H) (he : e ∈ c.atlas) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └─────────┘ ┴ └────┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘
doc └─────────┘
375 @local_homeomorph M H c.to_topological_space _ :=
id └──────────────┘ ┴ ┴ ┴└───────────────────┘
src └──────────────┘ └───────────────────┘
typ └──────────────┘ ┴ ┴ ┴└───────────────────┘
doc └──────────────┘ └───────────────────┘
376 { open_source := by convert c.open_source' he,
id └────────────┘ └┘
src └──────┘└────────────┘┴
typ └──────┘└────────────┘┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st └────────────────────────┘
377 open_target := by convert c.open_target he,
id └───────────┘ └┘
src └──────┘└───────────┘┴
typ └──────┘└───────────┘┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st └───────────────────────┘
378 continuous_to_fun := begin
st └─────
379 letI : topological_space M := c.to_topological_space,
id └───────────────┘ ┴ └────────────────────┘
src └─────┘└───────────────┘┴ └──┘└────────────────────┘
typ └─────┘└───────────────┘┴┴└──┘└────────────────────┘
doc └─────┘└───────────────┘┴ └──┘└────────────────────┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴└┘ ┴ └──┘
st ───────────────────────────────────────────────────────┘└─
380 rw continuous_on_open_iff (c.open_source' he),
id └────────────────────┘ └────────────┘ └┘
src └─┘└────────────────────┘┴ └────────────┘┴ ┴
typ └─┘└────────────────────┘┴ └────────────┘┴└┘┴
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└─
381 assume s s_open,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ──────────────────┘└─
382 rw inter_comm,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
383 apply topological_space.generate_open.basic,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────────────────────┘└─
384 simp only [exists_prop, mem_Union, mem_singleton_iff],
id └─────────┘ └───────┘ └───────────────┘
src └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘┴
typ └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────┘└─
385 exact ⟨e, he, ⟨s, s_open, rfl⟩⟩
id ┴ └┘ ┴ └────┘ └─┘
src └────┘ └┘ └┘ └┘ └┘└─┘└──
typ └────┘ ┴└┘└┘└┘ ┴└┘└────┘└┘└─┘└──
doc └────┘ └┘ └┘ └┘ └┘ └──
txt └────┘ └┘ └┘ └┘ └┘ └──
par └────┘ └┘ └┘ └┘ └┘ └──
pid ┴ └┘ └┘ └┘ └┘ └┘└
st ────────────────────────────────────
386 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
387 continuous_inv_fun := begin
st └─────
388 letI : topological_space M := c.to_topological_space,
id └───────────────┘ ┴ └────────────────────┘
src └─────┘└───────────────┘┴ └──┘└────────────────────┘
typ └─────┘└───────────────┘┴┴└──┘└────────────────────┘
doc └─────┘└───────────────┘┴ └──┘└────────────────────┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴└┘ ┴ └──┘
st ───────────────────────────────────────────────────────┘└─
389 apply continuous_on_open_of_generate_from (c.open_target he),
id └─────────────────────────────────┘ └───────────┘ └┘
src └────┘└─────────────────────────────────┘┴ └───────────┘┴ ┴
typ └────┘└─────────────────────────────────┘┴ └───────────┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└─
390 assume t ht,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
391 simp only [exists_prop, mem_Union, mem_singleton_iff] at ht,
id └─────────┘ └───────┘ └───────────────┘
src └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘└─────┘
typ └─────────┘└─────────┘└┘└───────┘└┘└───────────────┘└─────┘
doc └─────────┘ └┘ └┘ └─────┘
txt └─────────┘ └┘ └┘ └─────┘
par └─────────┘ └┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ └┘ ┴┴└───┘
st ──────────────────────────────────────────────────────────────┘└─
392 rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩,
id └┘
src └─────┘ └─────────────────────────────────┘
typ └─────┘└┘└─────────────────────────────────┘
doc └─────┘ └─────────────────────────────────┘
txt └─────┘ └─────────────────────────────────┘
par └─────┘ └─────────────────────────────────┘
pid ┴ └─────────────────────────────────┘
st ───────────────────────────────────────────────┘└─
393 rw ts,
id └┘
src └─┘
typ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
394 let f := e.symm.trans e',
id └──────────┘ └┘
src └───────┘└──────────┘┴
typ └───────┘└──────────┘┴└┘
doc └───────┘└──────────┘┴
txt └───────┘ ┴
par └───────┘ ┴
pid └───┘┴└─┘ ┴
st ───────────────────────────┘└─
395 have : is_open (f.to_fun ⁻¹' s ∩ f.source),
id └─────┘ └──────┘ └─┘ ┴ ┴ └──────┘
src └─────┘└─────┘┴ └──────┘┴└─┘┴ ┴┴┴└──────┘┴
typ └─────┘└─────┘┴ └──────┘┴└─┘┴┴┴┴┴└──────┘┴
doc └─────┘└─────┘┴ ┴└─┘┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────┘
396 by simpa [inter_comm] using (continuous_on_open_iff (c.open_source e e' he e'_atlas)).1
id └────────┘ └────────────────────┘ └───────────┘
src └─────┘└────────┘└──────┘ └────────────────────┘┴ └───────────┘┴ ┴ ┴ ┴ └────
typ └─────┘└────────┘└──────┘ └────────────────────┘┴ └───────────┘┴ ┴ ┴ ┴ └────
doc └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └────
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └────
par └─────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └────
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴ ┴ └────
397 (c.continuous_to_fun e e' he e'_atlas) s s_open,
id └─────────────────┘ ┴ └┘ └┘ └──────┘ ┴ └────┘
src ───────┘ └─────────────────┘┴ ┴ ┴ ┴ └┘ ┴
typ ───────┘ └─────────────────┘┴┴┴└┘┴└┘┴└──────┘└┘┴┴└────┘
doc ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ ┴ └┘ ┴
st └─
398 have A : e'.to_fun ∘ e.inv_fun ⁻¹' s ∩ (e.target ∩ e.inv_fun ⁻¹' e'.source) =
id ┴ ┴
src └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴└
typ └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴└
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
st ──────────────────────────────────────────────────────────────────────────────────
399 e.target ∩ (e'.to_fun ∘ e.inv_fun ⁻¹' s ∩ e.inv_fun ⁻¹' e'.source),
id └──────┘ └───────┘ ┴ └───────┘ └───────┘
src ────────────┘└──────┘┴ ┴ └───────┘┴ ┴ ┴ ┴ ┴ ┴└───────┘┴ ┴└───────┘┴
typ ────────────┘└──────┘┴ ┴ └───────┘┴ ┴ ┴ ┴┴┴ ┴└───────┘┴ ┴└───────┘┴
doc ────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘
400 by { rw [← inter_assoc, ← inter_assoc], congr' 1, exact inter_comm _ _ },
id └─────────┘ └─────────┘ └────────┘
src └────┘└─────────┘└──┘└─────────┘┴ └──────┘ └────┘└────────┘└───┘
typ └────┘└─────────┘└──┘└─────────┘┴ └──────┘ └────┘└────────┘└───┘
doc └────┘ └──┘ ┴ └──────┘ └────┘ └───┘
txt └────┘ └──┘ ┴ └──────┘ └────┘ └───┘
par └────┘ └──┘ ┴ └──────┘ └────┘ └───┘
pid └──┘ └──┘ ┴ ┴┴ ┴ └──┘┴
st ┴└────────────────┘└─────────────┘└─────────┘└─────────────────────┘└┘└
401 simpa [local_equiv.trans_source, preimage_inter, preimage_comp.symm, A] using this
id └──────────────────────┘ └────────────┘ ┴ └──┘
src └─────┘└──────────────────────┘└┘└────────────┘└┘ └┘ └──────┘ └
typ └─────┘└──────────────────────┘└┘└────────────┘└┘└────────────────┘└┘┴└──────┘└──┘└
doc └─────┘ └┘ └┘ └┘ └──────┘ └
txt └─────┘ └┘ └┘ └┘ └──────┘ └
par └─────┘ └┘ └┘ └┘ └──────┘ └
pid ┴┴ └┘ └┘ └┘ ┴┴└────┘ └
st ───────────────────────────────────────────────────────────────────────────────────────
402 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
403 ..e }
id ┴
typ ┴
404
405 def to_manifold : @manifold H _ M c.to_topological_space :=
id └──────┘ ┴ ┴ ┴└───────────────────┘
src └──────┘ └───────────────────┘
typ └──────┘ ┴ ┴ ┴└───────────────────┘
doc └──────┘ └───────────────────┘
406 { atlas := ⋃ (e : local_equiv M H) (he : e ∈ c.atlas), {c.local_homeomorph e he},
id ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴┴└───────────────┘ ┴ └┘
src ┴ └─────────┘ ┴ └────┘ ┴ ┴ └───────────────┘
typ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴┴└───────────────┘ ┴ └┘
doc ┴ └─────────┘ ┴
407 chart_at := λx, c.local_homeomorph (c.chart_at x) (c.chart_mem_atlas x),
id ┴ ┴└───────────────┘ ┴└───────┘ ┴ ┴└──────────────┘ ┴
src └───────────────┘ └───────┘ └──────────────┘
typ ┴ ┴└───────────────┘ ┴└───────┘ ┴ ┴└──────────────┘ ┴
408 mem_chart_source := λx, c.mem_chart_source x,
id ┴ ┴└───────────────┘ ┴
src └───────────────┘
typ ┴ ┴└───────────────┘ ┴
409 chart_mem_atlas := λx, begin
id ┴
typ ┴
st └─────
410 simp only [mem_Union, mem_singleton_iff],
id └───────┘ └───────────────┘
src └─────────┘└───────┘└┘└───────────────┘┴
typ └─────────┘└───────┘└┘└───────────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───────────────────────────────────────────┘└─
411 exact ⟨c.chart_at x, c.chart_mem_atlas x, rfl⟩,
id └────────┘ └───────────────┘ ┴ └─┘
src └────┘ └────────┘┴ └┘└───────────────┘┴ └┘└─┘┴
typ └────┘ └────────┘┴ └┘└───────────────┘┴┴└┘└─┘┴
doc └────┘ ┴ └┘ ┴ └┘ ┴
txt └────┘ ┴ └┘ ┴ └┘ ┴
par └────┘ ┴ └┘ ┴ └┘ ┴
pid ┴ ┴ └┘ ┴ └┘ ┴
st ─────────────────────────────────────────────────┘└─
412 end }
st ────┘
413
414 end manifold_core
415
416 section has_groupoid
417 variables [topological_space H] [topological_space M] [manifold H M]
id └───────────────┘ └───────────────┘ └──────┘
src └───────────────┘ └───────────────┘ └──────┘
typ └───────────────┘ └───────────────┘ └──────┘
doc └───────────────┘ └───────────────┘ └──────┘
418
419 /-- A manifold has an atlas in a groupoid G if the change of coordinates belong to the groupoid -/
420 class has_groupoid {H : Type*} [topological_space H] (M : Type*) [topological_space M]
id └───┘ └───────────────┘ ┴ └───┘ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ └───┘ └───────────────┘ ┴ └───┘ └───────────────┘ ┴
doc └───────────────┘ └───────────────┘
421 [manifold H M] (G : structure_groupoid H) : Prop :=
id └──────┘ ┴ ┴ └────────────────┘ ┴
src └──────┘ └────────────────┘
typ └──────┘ ┴ ┴ └────────────────┘ ┴
doc └──────┘ └────────────────┘
422 (compatible : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ G)
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴└───┘ └┘ └┘ ┴ ┴
src └──────────────┘ ┴ └───┘ ┴ └───┘ └───┘ └┘ ┴
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴└───┘ └┘ └┘ ┴ ┴
doc └──────────────┘ └───┘ └┘
423
424 lemma has_groupoid_of_le {G₁ G₂ : structure_groupoid H} (h : has_groupoid M G₁) (hle : G₁ ≤ G₂) :
id └────────────────┘ ┴ └──────────┘ ┴ └┘ └┘ ┴ └┘
src └────────────────┘ └──────────┘ ┴
typ └────────────────┘ ┴ └──────────┘ ┴ └┘ └┘ ┴ └┘
doc └────────────────┘ └──────────┘
425 has_groupoid M G₂ :=
id └──────────┘ ┴ └┘
src └──────────┘
typ └──────────┘ ┴ └┘
doc └──────────┘
426 ⟨ λ e e' he he', hle ((h.compatible : _) he he') ⟩
id ┴ └┘ └┘ └─┘ └─┘ ┴└─────────┘ └┘ └─┘
src └─────────┘
typ ┴ └┘ └┘ └─┘ └─┘ ┴└─────────┘ └┘ └─┘
427
428 lemma has_groupoid_of_pregroupoid (PG : pregroupoid H)
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
429 (h : ∀{e e' : local_homeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M
id └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴
src └──────────────┘ ┴ └───┘ ┴ └───┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴
doc └──────────────┘
430 → PG.property (e.symm ≫ₕ e').to_fun (e.symm ≫ₕ e').source) :
id └┘└───────┘ ┴└───┘ └┘ └┘ └────┘ ┴└───┘ └┘ └┘ └────┘
src └───────┘ └───┘ └┘ └────┘ └───┘ └┘ └────┘
typ └┘└───────┘ ┴└───┘ └┘ └┘ └────┘ ┴└───┘ └┘ └┘ └────┘
doc └───┘ └┘ └───┘ └┘
431 has_groupoid M (PG.groupoid) :=
id └──────────┘ ┴ └┘└───────┘
src └──────────┘ └───────┘
typ └──────────┘ ┴ └┘└───────┘
doc └──────────┘ └───────┘
432 ⟨assume e e' he he', (mem_groupoid_of_pregroupoid PG _).mpr ⟨h he he', h he' he⟩⟩
id ┴ └┘ └┘ └─┘ └─────────────────────────┘ └┘ └─┘ ┴ └┘ └─┘ ┴ └─┘ └┘
src └─────────────────────────┘ └─┘
typ ┴ └┘ └┘ └─┘ └─────────────────────────┘ └┘ └─┘ ┴ └┘ └─┘ ┴ └─┘ └┘
433
434 /-- The trivial manifold structure on the model space is compatible with any groupoid -/
435 instance has_groupoid_model_space (H : Type*) [topological_space H] (G : structure_groupoid H) :
id └───────────────┘ ┴ └────────────────┘ ┴
src └───────────────┘ └────────────────┘
typ └───────────────┘ ┴ └────────────────┘ ┴
doc └───────────────┘ └────────────────┘
436 has_groupoid H G :=
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
doc └──────────┘
437 { compatible := λe e' he he', begin
id ┴ └┘ └┘ └─┘
typ ┴ └┘ └┘ └─┘
st └─────
438 replace he : e ∈ atlas H H := he,
id ┴ ┴ └───┘ ┴ └┘
src └───────────┘ ┴┴┴└───┘┴ ┴ └──┘
typ └───────────┘┴┴┴┴└───┘┴ ┴┴└──┘└┘
doc └───────────┘ ┴ ┴ ┴ ┴ └──┘
txt └───────────┘ ┴ ┴ ┴ ┴ └──┘
par └───────────┘ ┴ ┴ ┴ ┴ └──┘
pid └─┘└─┘ ┴ ┴ ┴ ┴ └──┘
st ───────────────────────────────────┘└─
439 replace he' : e' ∈ atlas H H := he',
id └┘ └───┘ ┴ └─┘
src └────────────┘ ┴ ┴└───┘┴ ┴ └──┘
typ └────────────┘└┘┴ ┴└───┘┴ ┴┴└──┘└─┘
doc └────────────┘ ┴ ┴ ┴ ┴ └──┘
txt └────────────┘ ┴ ┴ ┴ ┴ └──┘
par └────────────┘ ┴ ┴ ┴ ┴ └──┘
pid └──┘└─┘ ┴ ┴ ┴ ┴ └──┘
st ──────────────────────────────────────┘└─
440 rw model_space_atlas at he he',
id └───────────────┘
src └─┘└───────────────┘└────────┘
typ └─┘└───────────────┘└────────┘
doc └─┘└───────────────┘└────────┘
txt └─┘ └────────┘
par └─┘ └────────┘
pid ┴ └────────┘
st ─────────────────────────────────┘└─
441 simp [he, he', structure_groupoid.id_mem]
id └┘ └─┘ └───────────────────────┘
src └────┘ └┘ └┘└───────────────────────┘└─
typ └────┘└┘└┘└─┘└┘└───────────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ──────────────────────────────────────────────
442 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
443
444 /-- Any manifold structure is compatible with the groupoid of all local homeomorphisms -/
445 instance has_groupoid_continuous_groupoid : has_groupoid M (continuous_groupoid H) :=
id └──────────┘ ┴ └─────────────────┘ ┴
src └──────────┘ └─────────────────┘
typ └──────────┘ ┴ └─────────────────┘ ┴
doc └──────────┘ └─────────────────┘
446 ⟨begin
st └─────
447 assume e e' he he',
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ───────────────────┘└─
448 rw [continuous_groupoid, mem_groupoid_of_pregroupoid],
id └─────────────────┘ └─────────────────────────┘
src └──┘└─────────────────┘└┘└─────────────────────────┘┴
typ └──┘└─────────────────┘└┘└─────────────────────────┘┴
doc └──┘└─────────────────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────┘└───────────────────────────┘└──
449 simp only [and_self]
id └──────┘
src └─────────┘└──────┘└┘
typ └─────────┘└──────┘└┘
doc └─────────┘ └┘
txt └─────────┘ └┘
par └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ──────────────────────┘
450 end⟩
st └─┘
451
452 /-- A G-diffeomorphism between two manifolds is a homeomorphism which, when read in the charts,
453 belongs to G. We avoid the word diffeomorph as it is too related to the smooth category, and use
454 structomorph instead. -/
455 structure structomorph (G : structure_groupoid H) (M : Type*) (M' : Type*)
id └────────────────┘ ┴ └───┘ └───┘
src └────────────────┘
typ └────────────────┘ ┴ └───┘ └───┘
doc └────────────────┘
456 [topological_space M] [topological_space M'] [manifold H M] [manifold H M']
id └───────────────┘ ┴ └───────────────┘ └┘ └──────┘ ┴ ┴ └──────┘ ┴ └┘
src └───────────────┘ └───────────────┘ └──────┘ └──────┘
typ └───────────────┘ ┴ └───────────────┘ └┘ └──────┘ ┴ ┴ └──────┘ ┴ └┘
doc └───────────────┘ └───────────────┘ └──────┘ └──────┘
457 extends homeomorph M M' :=
id └────────┘ ┴ └┘
src └────────┘
typ └────────┘ ┴ └┘
doc └────────┘
458 (to_fun_mem_groupoid : ∀c : local_homeomorph M H, ∀c' : local_homeomorph M' H,
id ┴ └──────────────┘ ┴ ┴ └──────────────┘ └┘ ┴
src └──────────────┘ └──────────────┘
typ ┴ └──────────────┘ ┴ ┴ └──────────────┘ └┘ ┴
doc └──────────────┘ └──────────────┘
459 c ∈ atlas H M → c' ∈ atlas H M' → c.symm ≫ₕ to_homeomorph.to_local_homeomorph ≫ₕ c' ∈ G)
id ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ └┘ ┴└───┘ └┘ └───────────┘└──────────────────┘ └┘ └┘ ┴ ┴
src ┴ └───┘ ┴ └───┘ └───┘ └┘ └──────────────────┘ └┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ └───┘ ┴ └┘ ┴└───┘ └┘ └───────────┘└──────────────────┘ └┘ └┘ ┴ ┴
doc └───┘ └┘ └──────────────────┘ └┘
460
461 variables [topological_space M'] [topological_space M'']
id └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘
462 {G : structure_groupoid H} [manifold H M'] [manifold H M'']
id └────────────────┘ └──────┘ └──────┘
src └────────────────┘ └──────┘ └──────┘
typ └────────────────┘ └──────┘ └──────┘
doc └────────────────┘ └──────┘ └──────┘
463
464 /-- The identity is a diffeomorphism of any manifold, for any groupoid. -/
465 def structomorph.refl (M : Type*) [topological_space M] [manifold H M]
id └───────────────┘ ┴ └──────┘ ┴ ┴
src └───────────────┘ └──────┘
typ └───────────────┘ ┴ └──────┘ ┴ ┴
doc └───────────────┘ └──────┘
466 [has_groupoid M G] : structomorph G M M :=
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
467 { to_fun_mem_groupoid := λc c' hc hc', begin
id ┴ └┘ └┘ └─┘
typ ┴ └┘ └┘ └─┘
st └─────
468 change (local_homeomorph.symm c) ≫ₕ (local_homeomorph.refl M) ≫ₕ c' ∈ G,
id └───────────────────┘ ┴ └┘ └───────────────────┘ ┴ └┘ ┴ ┴
src └─────┘ └───────────────────┘┴ └┘└┘┴ └───────────────────┘┴ └┘ ┴ ┴┴┴
typ └─────┘ └───────────────────┘┴┴└┘└┘┴ └───────────────────┘┴┴└┘ ┴└┘┴┴┴┴
doc └─────┘ └───────────────────┘┴ └┘└┘┴ └───────────────────┘┴ └┘ ┴ ┴ ┴
txt └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
469 rw local_homeomorph.refl_trans,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────┘└─
470 exact has_groupoid.compatible G hc hc'
id └─────────────────────┘ ┴ └┘ └─┘
src └────┘└─────────────────────┘┴ ┴ ┴ └
typ └────┘└─────────────────────┘┴┴┴└┘┴└─┘└
doc └────┘ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────
471 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
472 ..homeomorph.refl M }
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
473
474 /-- The inverse of a structomorphism is a structomorphism -/
475 def structomorph.symm (e : structomorph G M M') : structomorph G M' M :=
id └──────────┘ ┴ ┴ └┘ └──────────┘ ┴ └┘ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └┘ └──────────┘ ┴ └┘ ┴
doc └──────────┘ └──────────┘
476 { to_fun_mem_groupoid := begin
st └─────
477 assume c c' hc hc',
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ─────────────────────┘└─
478 have : (c'.symm ≫ₕ e.to_homeomorph.to_local_homeomorph ≫ₕ c).symm ∈ G :=
id └─────┘ └┘ └─────────────────────────────────┘ ┴ ┴ ┴
src └─────┘ └─────┘┴└┘┴└─────────────────────────────────┘┴ ┴ └─────┘┴┴ └───
typ └─────┘ └─────┘┴└┘┴└─────────────────────────────────┘┴ ┴┴└─────┘┴┴┴└───
doc └─────┘ └─────┘┴└┘┴└─────────────────────────────────┘┴ ┴ └─────┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────
479 G.inv _ (e.to_fun_mem_groupoid c' c hc' hc),
id └───┘ └───────────────────┘ └┘ ┴ └─┘ └┘
src ─────┘└───┘└─┘ └───────────────────┘┴ ┴ ┴ ┴ ┴
typ ─────┘└───┘└─┘ └───────────────────┘┴└┘┴┴┴└─┘┴└┘┴
doc ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
txt ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
par ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└─
480 simp at this,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└─────┘
st ───────────────┘└─
481 rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
id └───────────────────────────┘ └───────────────────────────┘ └───────┘ └─────────┘
src └───┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────┘└┘└─────────┘└─
typ └───┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────┘└┘└─────────┘└─
doc └───┘ └┘ └┘ └┘ └─
txt └───┘ └┘ └┘ └┘ └─
par └───┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st ─────────────────────────────────────┘└─────────────────────────────┘└─────────┘└───────────┘┴└
482 at this,
src ────────────┘
typ ────────────┘
doc ────────────┘
txt ────────────┘
par ────────────┘
pid ────────────┘
st ────────────┘└─
483 end,
st ────┘
484 ..e.to_homeomorph.symm}
id ┴└────────────┘└───┘
src └────────────┘└───┘
typ ┴└────────────┘└───┘
485
486 /-- The composition of structomorphisms is a structomorphism -/
487 def structomorph.trans (e : structomorph G M M') (e' : structomorph G M' M'') : structomorph G M M'' :=
id └──────────┘ ┴ ┴ └┘ └──────────┘ ┴ └┘ └─┘ └──────────┘ ┴ ┴ └─┘
src └──────────┘ └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └┘ └──────────┘ ┴ └┘ └─┘ └──────────┘ ┴ ┴ └─┘
doc └──────────┘ └──────────┘ └──────────┘
488 { to_fun_mem_groupoid := begin
st └─────
489 /- Let c and c' be two charts in M and M''. We want to show that e' ∘ e is smooth in these
st ───────────────────────────────────────────────────────────────────────────────────────────────
490 charts, around any point x. For this, let y = e (c⁻¹ x), and consider a chart g around y.
st ──────────────────────────────────────────────────────────────────────────────────────────────
491 Then g ∘ e ∘ c⁻¹ and c' ∘ e' ∘ g⁻¹ are both smooth as e and e' are structomorphisms, so
st ────────────────────────────────────────────────────────────────────────────────────────────
492 their composition is smooth, and it coincides with c' ∘ e' ∘ e ∘ c⁻¹ around x. -/
st ──────────────────────────────────────────────────────────────────────────────────────
493 assume c c' hc hc',
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ─────────────────────┘└─
494 refine G.locality _ (λx hx, _),
id └────────┘
src └─────┘└────────┘└─┘ └──────┘
typ └─────┘└────────┘└─┘ └──────┘
doc └─────┘ └─┘ └──────┘
txt └─────┘ └─┘ └──────┘
par └─────┘ └─┘ └──────┘
pid ┴ └─┘ └──────┘
st ─────────────────────────────────┘└─
495 let f₁ := e.to_homeomorph.to_local_homeomorph,
id └─────────────────────────────────┘
src └────────┘└─────────────────────────────────┘
typ └────────┘└─────────────────────────────────┘
doc └────────┘└─────────────────────────────────┘
txt └────────┘
par └────────┘
pid └────┘┴└─┘
st ────────────────────────────────────────────────┘└─
496 let f₂ := e'.to_homeomorph.to_local_homeomorph,
id └──────────────────────────────────┘
src └────────┘└──────────────────────────────────┘
typ └────────┘└──────────────────────────────────┘
doc └────────┘└──────────────────────────────────┘
txt └────────┘
par └────────┘
pid └────┘┴└─┘
st ─────────────────────────────────────────────────┘└─
497 let f := (e.to_homeomorph.trans e'.to_homeomorph).to_local_homeomorph,
id └───────────────────┘ └──────────────┘
src └────────┘ └───────────────────┘┴└──────────────┘└───────────────────┘
typ └────────┘ └───────────────────┘┴└──────────────┘└───────────────────┘
doc └────────┘ ┴ └───────────────────┘
txt └────────┘ ┴ └───────────────────┘
par └────────┘ ┴ └───────────────────┘
pid └───┘└┘└─┘ ┴ └──────────────────┘┴
st ─────────────────────────────────────────────────────────────────────────┘└─
498 have feq : f = f₁ ≫ₕ f₂ := homeomorph.trans_to_local_homeomorph _ _,
id ┴ ┴ └┘ └┘ └┘ └──────────────────────────────────┘
src └─────────┘ ┴┴┴ ┴└┘┴ └──┘└──────────────────────────────────┘└──┘
typ └─────────┘┴┴┴┴└┘┴└┘┴└┘└──┘└──────────────────────────────────┘└──┘
doc └─────────┘ ┴ ┴ ┴└┘┴ └──┘ └──┘
txt └─────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘
par └─────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └──┘ └──┘
st ──────────────────────────────────────────────────────────────────────┘└─
499 -- define the atlas g around y
st ───────────────────────────────────
500 let y := (c.symm ≫ₕ f₁).to_fun x,
id └────┘ └┘ ┴
src └───────┘ └────┘┴ ┴ └───────┘
typ └───────┘ └────┘┴ ┴└┘└───────┘┴
doc └───────┘ └────┘┴ ┴ └───────┘
txt └───────┘ ┴ ┴ └───────┘
par └───────┘ ┴ ┴ └───────┘
pid └───┘┴└─┘ ┴ ┴ └───────┘
st ───────────────────────────────────┘└─
501 let g := chart_at H y,
id └──────┘ ┴ ┴
src └───────┘└──────┘┴ ┴
typ └───────┘└──────┘┴┴┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴
st ────────────────────────┘└─
502 have hg₁ := chart_mem_atlas H y,
id └─────────────┘ ┴ ┴
src └──────────┘└─────────────┘┴ ┴
typ └──────────┘└─────────────┘┴┴┴┴
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴
st ──────────────────────────────────┘└─
503 have hg₂ := mem_chart_source H y,
id └──────────────┘ ┴ ┴
src └──────────┘└──────────────┘┴ ┴
typ └──────────┘└──────────────┘┴┴┴┴
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴
st ───────────────────────────────────┘└─
504 let s := (c.symm ≫ₕ f₁).source ∩ (c.symm ≫ₕ f₁).to_fun ⁻¹' g.source,
id ┴ └────┘ └┘ └─┘ └──────┘
src └───────┘ ┴ ┴ └───────┘┴┴ └────┘┴ ┴ └───────┘└─┘┴└──────┘
typ └───────┘ ┴ ┴ └───────┘┴┴ └────┘┴ ┴└┘└───────┘└─┘┴└──────┘
doc └───────┘ ┴ ┴ └───────┘ ┴ └────┘┴ ┴ └───────┘└─┘┴
txt └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴
par └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴
pid └───┘┴└─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
505 have open_s : is_open s,
id └─────┘ ┴
src └────────────┘└─────┘┴
typ └────────────┘└─────┘┴┴
doc └────────────┘└─────┘┴
txt └────────────┘ ┴
par └────────────┘ ┴
pid └─────────┘└─┘ ┴
st ──────────────────────────┘
506 by apply (c.symm ≫ₕ f₁).continuous_to_fun.preimage_open_of_open; apply open_source,
id └────┘ └┘ └─────────┘
src └────┘ └────┘┴ ┴ └───────────────────────────────────────┘ └────┘└─────────┘
typ └────┘ └────┘┴ ┴└┘└───────────────────────────────────────┘ └────┘└─────────┘
doc └────┘ └────┘┴ ┴ └───────────────────────────────────────┘ └────┘
txt └────┘ ┴ ┴ └───────────────────────────────────────┘ └────┘
par └────┘ ┴ ┴ └───────────────────────────────────────┘ └────┘
pid ┴ ┴ ┴ └──────────────────────────────────────┘┴ ┴
st └─
507 have : x ∈ s,
id ┴ ┴ ┴
src └─────┘ ┴┴┴
typ └─────┘┴┴┴┴┴
doc └─────┘ ┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴
st ───────────────┘└─
508 { split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ─────┘└───┘└─
509 { simp only [trans_source, preimage_univ, inter_univ, homeomorph.to_local_homeomorph_source],
id └──────────┘ └───────────┘ └────────┘ └───────────────────────────────────┘
src └─────────┘└──────────┘└┘└───────────┘└┘└────────┘└┘└───────────────────────────────────┘┴
typ └─────────┘└──────────┘└┘└───────────┘└┘└────────┘└┘└───────────────────────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ───────┘└────────────────────────────────────────────────────────────────────────────────────────┘└─
510 rw trans_source at hx,
id └──────────┘
src └─┘└──────────┘└────┘
typ └─┘└──────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────────────────┘└─
511 exact hx.1 },
id └┘
src └────┘ └─┘
typ └────┘└┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────────┘└┘└
512 { exact hg₂ } },
id └─┘
src └────┘ ┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────┘└──┘└
513 refine ⟨s, open_s, ⟨this, _⟩⟩,
id ┴ └────┘ └──┘
src └─────┘ └┘ └┘ └───┘
typ └─────┘ ┴└┘└────┘└┘ └──┘└───┘
doc └─────┘ └┘ └┘ └───┘
txt └─────┘ └┘ └┘ └───┘
par └─────┘ └┘ └┘ └───┘
pid ┴ └┘ └┘ └───┘
st ────────────────────────────────┘└─
514 let F₁ := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ (g.symm ≫ₕ f₂ ≫ₕ c'),
id └────┘ └┘ └────┘ └┘ └┘
src └────────┘ └────┘┴ ┴ ┴ ┴ └┘ ┴ └────┘┴ ┴ ┴ ┴ ┴
typ └────────┘ └────┘┴ ┴└┘┴ ┴ └┘ ┴ └────┘┴ ┴└┘┴ ┴└┘┴
doc └────────┘ └────┘┴ ┴ ┴ ┴ └┘ ┴ └────┘┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
515 have A : F₁ ∈ G :=
id └┘ ┴
src └───────┘ ┴ ┴ └───
typ └───────┘└┘┴ ┴┴└───
doc └───────┘ ┴ ┴ └───
txt └───────┘ ┴ ┴ └───
par └───────┘ ┴ ┴ └───
pid └────┘└─┘ ┴ ┴ └───
st ───────────────────────
516 G.comp _ _ (e.to_fun_mem_groupoid c g hc hg₁) (e'.to_fun_mem_groupoid g c' hg₁ hc'),
id └────┘ └───────────────────┘ ┴ └┘ └────────────────────┘ ┴ └┘ └─┘ └─┘
src ─────┘└────┘└───┘ └───────────────────┘┴ ┴ ┴ ┴ └┘ └────────────────────┘┴ ┴ ┴ ┴ ┴
typ ─────┘└────┘└───┘ └───────────────────┘┴┴┴ ┴└┘┴ └┘ └────────────────────┘┴┴┴└┘┴└─┘┴└─┘┴
doc ─────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
txt ─────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par ─────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid ─────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
517 let F₂ := (c.symm ≫ₕ f ≫ₕ c').restr s,
id └────┘ ┴ └┘ ┴
src └────────┘ └────┘┴ ┴ ┴ ┴ └──────┘
typ └────────┘ └────┘┴ ┴┴┴ ┴└┘└──────┘┴
doc └────────┘ └────┘┴ ┴ ┴ ┴ └──────┘
txt └────────┘ ┴ ┴ ┴ ┴ └──────┘
par └────────┘ ┴ ┴ ┴ ┴ └──────┘
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ └──────┘
st ────────────────────────────────────────┘└─
518 have : F₁ ≈ F₂ := calc
id └┘ ┴ └┘
src └─────┘ ┴┴┴ └──┘ └
typ └─────┘└┘┴┴┴└┘└──┘ └
doc └─────┘ ┴ ┴ └──┘ └
txt └─────┘ ┴ ┴ └──┘ └
par └─────┘ ┴ ┴ └──┘ └
pid └───┘└┘ ┴ ┴ └──┘ └
st ───────────────────────────
519 F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' : by simp [F₁, trans_assoc]
id └┘ └────┘ └┘ └────┘ └┘ └┘ └┘ └─────────┘
src ─────┘ ┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└────┘└┘ ┴ ┴ ┴ └─┘ ┴└────┘ └┘└─────────┘└─
typ ─────┘└┘┴ ┴└────┘┴ ┴└┘┴ ┴ ┴ ┴└────┘└┘ ┴└┘┴ ┴└┘└─┘ ┴└────┘└┘└┘└─────────┘└─
doc ─────┘ ┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└────┘└┘ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ └─────┘ └┘ └─
st ────────────────────────────────────────────────────────┘└───────────────────────
520 ... ≈ c.symm ≫ₕ f₁ ≫ₕ (of_set g.source g.open_source) ≫ₕ f₂ ≫ₕ c' :
id └────┘ └──────┘ └───────────┘
src ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └────┘┴└──────┘┴└───────────┘└┘ ┴ ┴ ┴ └──
typ ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └────┘┴└──────┘┴└───────────┘└┘ ┴ ┴ ┴ └──
doc ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘ ┴ ┴ ┴ └──
txt ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ─────┘└───────────────────────────────────────────────────────────────────
521 by simp [eq_on_source_trans, trans_self_symm g]
id └────────────────┘ └─────────────┘ ┴
src ───────┘ ┴└────┘└────────────────┘└┘└─────────────┘┴ └─
typ ───────┘ ┴└────┘└────────────────┘└┘└─────────────┘┴┴└─
doc ───────┘ ┴└────┘└────────────────┘└┘└─────────────┘┴ └─
txt ───────┘ ┴└────┘ └┘ ┴ └─
par ───────┘ ┴└────┘ └┘ ┴ └─
pid ───────┘ └─────┘ └┘ ┴ └─
st ─────────┘└─────────────────────────────────────────────
522 ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (of_set g.source g.open_source)) ≫ₕ (f₂ ≫ₕ c') :
src ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
typ ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
doc ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
txt ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
par ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
pid ─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───
st ─────┘└─────────────────────────────────────────────────────────────────────────
523 by simp [trans_assoc]
id └─────────┘
src ───────┘ ┴└────┘└─────────┘└─
typ ───────┘ ┴└────┘└─────────┘└─
doc ───────┘ ┴└────┘ └─
txt ───────┘ ┴└────┘ └─
par ───────┘ ┴└────┘ └─
pid ───────┘ └─────┘ └─
st ─────────┘└───────────────────
524 ... ≈ ((c.symm ≫ₕ f₁).restr s) ≫ₕ (f₂ ≫ₕ c') : by simp [s, trans_of_set']
id ┴ ┴ └───────────┘
src ─────┘└──┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ └──┘ ┴└────┘ └┘└───────────┘└─
typ ─────┘└──┘ ┴ ┴ ┴ └──────┘┴└┘ ┴ ┴ ┴ └──┘ ┴└────┘┴└┘└───────────┘└─
doc ─────┘└──┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └─
txt ─────┘└──┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └─
par ─────┘└──┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ └──┘ ┴└────┘ └┘ └─
pid ─────────┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ └──┘ └─────┘ └┘ └─
st ─────┘└───────────────────────────────────────────────┘└────────────────────────
525 ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (f₂ ≫ₕ c')).restr s : by simp [restr_trans]
id └─────────┘
src ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ ┴└────┘└─────────┘└─
typ ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ ┴└────┘└─────────┘└─
doc ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ ┴└────┘ └─
txt ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ ┴└────┘ └─
par ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ ┴└────┘ └─
pid ─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘ └─────┘ └─
st ─────┘└───────────────────────────────────────────────┘└───────────────────
526 ... ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s : by simp [eq_on_source_restr, trans_assoc]
id └────────────────┘ └─────────┘
src ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ ┴└────┘└────────────────┘└┘└─────────┘└─
typ ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ ┴└────┘└────────────────┘└┘└─────────┘└─
doc ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ ┴└────┘└────────────────┘└┘ └─
txt ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ ┴└────┘ └┘ └─
par ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ ┴└────┘ └┘ └─
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──────┘ └─┘ └─────┘ └┘ └─
st ─────┘└─────────────────────────────────────────────┘└───────────────────────────────────────
527 ... ≈ F₂ : by simp [F₂, feq],
id └┘ └┘ └─┘
src ─────┘└──┘ ┴ └─┘ ┴└────┘ └┘ ┴
typ ─────┘└──┘ ┴└┘└─┘ ┴└────┘└┘└┘└─┘┴
doc ─────┘└──┘ ┴ └─┘ ┴└────┘ └┘ ┴
txt ─────┘└──┘ ┴ └─┘ ┴└────┘ └┘ ┴
par ─────┘└──┘ ┴ └─┘ ┴└────┘ └┘ ┴
pid ─────────┘ ┴ └─┘ └─────┘ └┘ ┴
st ─────┘└───────────┘└─────────────┘└─
528 have : F₂ ∈ G := G.eq_on_source F₁ F₂ A (setoid.symm this),
id └┘ ┴ └────────────┘ └┘ └┘ ┴ └─────────┘ └──┘
src └─────┘ ┴ ┴ └──┘└────────────┘┴ ┴ ┴ ┴ └─────────┘┴ ┴
typ └─────┘└┘┴ ┴┴└──┘└────────────┘┴└┘┴└┘┴┴┴ └─────────┘┴└──┘┴
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
529 exact this
id └──┘
src └────┘ └
typ └────┘└──┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ───────────────
530 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
531 ..homeomorph.trans e.to_homeomorph e'.to_homeomorph }
id └──────────────┘ ┴└────────────┘ └┘└────────────┘
src └──────────────┘ └────────────┘ └────────────┘
typ └──────────────┘ ┴└────────────┘ └┘└────────────┘
532
533 end has_groupoid